$\forall$$r$:CRng, $p$:Ideal($r$)\{i\}, $d$:detach\_fun($\mid$$r$$\mid$;$p$), $F$:($\mid$$r$ / $d$$\mid\rightarrow\mathbb{P}$).
\\[0ex]($\forall$$w$:$\mid$$r$ / $d$$\mid$. SqStable($F$($w$))) $\Rightarrow$ (($\forall$$w$:$\mid$$r$ / $d$$\mid$. $F$($w$)) $\Leftarrow\!\Rightarrow$ ($\forall$$w$:$\mid$$r$$\mid$. $F$([$w$]\{$\mid$$r$ / $d$$\mid$\})))